Inference at * 1 1 
Iof proof for Lemma fun with inv is bij:



1. A : Type
2. B : Type
3. f : AB
4. g : BA
5. (g o f) = Id{A}
6. (f o g) = Id{B}
  Bij(A;B;f) 

latex

 by ((((Repeat (Unfolds ``biject inject surject`` 0)) 
CollapseTHEN (GenUnivCD))) 

CoCollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
C) inil_term))) 

latex

C1: 

C1: 7. a1 : A
C1: 8. a2 : A
C1: 9. f(a1) = f(a2)
C1:   a1 = a2
C2: 

C2: 7. b : B
C2:   a:A. (f(a) = b)
C.

Definitions

, t  T, P  Q, x:A. B(x), Surj(A;B;f), Inj(A;B;f), P & Q, Bij(A;B;f)